PRISM
=====
Version: 4.5.dev
Date: Sat Apr 03 03:44:48 CEST 2021
Hostname: christopher
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 pnueli-zuck.60.prism pnueli-zuck.props --property live
Parsing model file "pnueli-zuck.60.prism"...
Type: MDP
Modules: process0 process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15 process16 process17 process18 process19 process20 process21 process22 process23 process24 process25 process26 process27 process28 process29 process30 process31 process32 process33 process34 process35 process36 process37 process38 process39 process40 process41 process42 process43 process44 process45 process46 process47 process48 process49 process50 process51 process52 process53 process54 process55 process56 process57 process58 process59
Variables: p0 p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15 p16 p17 p18 p19 p20 p21 p22 p23 p24 p25 p26 p27 p28 p29 p30 p31 p32 p33 p34 p35 p36 p37 p38 p39 p40 p41 p42 p43 p44 p45 p46 p47 p48 p49 p50 p51 p52 p53 p54 p55 p56 p57 p58 p59
Parsing properties file "pnueli-zuck.props"...
1 property:
(1) "live": Pmax=? [ F (p1=10) ]
---------------------------------------------------------------------
Model checking: "live": Pmax=? [ F (p1=10) ]
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Computing reachable states...
Reachability (BFS): 423 iterations in 534.29 seconds (average 1.263095, setup 0.00)
Time for model construction: 542.501 seconds.
Type: MDP
States: 3.7E61 (1 initial)
Transitions: 2.875200000000002E63
Choices: 2.656800000000002E63
Transition matrix: 794686 nodes (3 terminal), 2.875200000000002E63 minterms, vars: 240r/240c/60nd
Warning: Switching to MTBDD engine, as number of states is too large for Sparse engine.
CUDD internal error detected, from the following stack trace:
jdd.JDD.ptrToNode(JDD.java:1718)
mtbdd.PrismMTBDD.Prob0A(PrismMTBDD.java:391)
prism.NondetModelChecker.computeUntilProbs(NondetModelChecker.java:1914)
prism.NondetModelChecker.checkProbUntil(NondetModelChecker.java:1185)
prism.NondetModelChecker.checkProbUntil(NondetModelChecker.java:1109)
prism.NondetModelChecker.checkProbPathFormulaSimple(NondetModelChecker.java:949)
prism.NondetModelChecker.checkProbPathFormula(NondetModelChecker.java:911)
prism.NondetModelChecker.checkExpressionProb(NondetModelChecker.java:271)
prism.NondetModelChecker.checkExpressionProb(NondetModelChecker.java:240)
prism.NondetModelChecker.checkExpression(NondetModelChecker.java:163)
prism.StateModelChecker.checkExpressionFilter(StateModelChecker.java:1174)
prism.StateModelChecker.checkExpression(StateModelChecker.java:311)
prism.NonProbModelChecker.checkExpression(NonProbModelChecker.java:80)
prism.NondetModelChecker.checkExpression(NondetModelChecker.java:182)
prism.StateModelChecker.check(StateModelChecker.java:237)
prism.Prism.modelCheck(Prism.java:3082)
prism.PrismCL.run(PrismCL.java:394)
prism.PrismCL.go(PrismCL.java:220)
prism.PrismCL.main(PrismCL.java:2641)
Overall running time: 928.952 seconds.
Error: Out of memory (or other internal error) in the CUDD library.
Tip: Try using the -cuddmaxmem switch to increase the memory available to CUDD.